/*!
 * \file set_relation.h
 *
 * \brief Declarations for the set and relation classes and classes
 *        they contain.
 *
 * The Set and Relation classes represent integer tuple sets
 * and relations with affine inequality and equality constraints and
 * equality constraints with uninterpreted function symbols.
 *
 * \date Started: 6/8/2010
 * \date Last Modified: 7/13/2010
 * \authors Alan LaMielle
 * \authors Ian Craig
 *
 * Copyright (c) 2010, Colorado State University <br>
 * All rights reserved. <br>
 * See ../../COPYING for details. <br>
 */

#ifndef SET_RELATION_H_
#define SET_RELATION_H_

#include <iegenlib/iegenlib.h>

#include <map>
using std::map;
#include <utility>
using std::pair;
#include <string>
using std::string;
#include <set>
using std::set;
#include <list>
using std::list;
#include <vector>
using std::vector;
#include <utility>

namespace iegenlib{

class Relation;

/*!
 * \class SRConstraint
 * \brief Base class for representing equality and inequality constraints
 */
class SRConstraint{
public:
  /*!
   * Boolean operator less than which will test the two constraint's expressions
   * against each other
   * @return bool true if this constraint's expression is less than the other,
   * otherwise false
   */
  inline const bool operator<(const SRConstraint& op2) const {
    return this->expr < op2.expr;
  }

  /*!
   * Boolean operator equal to which will test the two constraint's expressions
   * against each other.
   * @return bool true if this constraint's expression is equal to the other,
   * otherwise false
   */
  inline const bool operator==(const SRConstraint& op2) const {
    return this->expr == op2.expr;
  }

  ///Helper apply method for the visitor to visit the ExpVec in this constraint
  ///@param visitor Visitor that is traversing the strucure
  inline void applyExpVec(SRVisitor* visitor) const { expr.apply(visitor); }

  ///@return ExpVec associated with this Equality
  inline ExpVec getExpVec() const { return expr; }

  /*!
   * Determine if any coefficients of the given type are non-zero.
   *
   * @param type the type of term to examine
   * @param pos output parameter, set to the position of the term if a non-zero
   *            is found
   * @param coeff output parameter, set to the value of the non-zero coefficient
   *              if one is found
   * @return true if any coefficients of the given type are non-zero, false otherwise.
   */
  bool any(SymType type,int& pos,int& coeff) const;

  /*!
   * Determine if any coefficients of the given type at the given position are
   * non-zero.
   *
   * @param type the type of term to examine
   * @param pos the position of the term to check for non-zero coefficients
   * @param sym_table the symbol table to use to recurse into UFCall parameters
   * @return true if any coefficients of the given type in the given position
   *         are non-zero, false otherwise.
   */
  bool any(SymType type,int pos,SymbolTable const*const sym_table=NULL) const;

  /*!
   * @return true if this constraint has only affine terms, false if it
   *         contains at least one UFS term.
   */
  bool isAffine() const{return this->expr.isAffine();}

protected:
  inline SRConstraint(ExpVec expr):expr(expr){}

  ///Expression Vector of the constraint expression
  ExpVec expr;
};

/*!
 * \class SREquality
 * \brief Class representing an equality
 *
 * All equalities are represented by Expression = 0
 */
class SREquality: public SRConstraint{
public:
  /*!
   * SREquality Constructor
   *
   * @param expr An expression vector that represents this equality
   */
  inline SREquality(ExpVec expr):SRConstraint(expr){this->expr.normalizeEquality();}

  ///Apply method used by the visitors to traverse the Set/Relation structure
  ///@param visitor Visitor that is traversing the structure
  void apply(SRVisitor* visitor) const;

  /*!
   * Replaces the existential at the given postiion with the given expression.
   *
   * @param sym_table the symbol table to use
   * @param exist_pos the position of the existential to replace
   * @param equal_exp the expression to replace the existential with
   * @return an equality constraint with the existential replaced
   */
  SREquality replaceExistential(SymbolTable* sym_table,int exist_pos,
                                ExpVec equal_exp) const;
};

/*!
 * \class SRInequality
 * \brief Class representing an inequality
 *
 * All Inequalities are represented by Expression >= 0
 */
class SRInequality: public SRConstraint{
public:
  /*!
   * SRInequality Constructor
   *
   * @param expr An expression vector that represents this inequality
   */
  inline SRInequality(ExpVec expr):SRConstraint(expr){}

  ///Apply method used by the visitors to traverse the Set/Relation structure
  ///@param visitor Visitor that is traversing the structure
  void apply(SRVisitor* visitor) const;

  /*!
   * Replaces the existential at the given postiion with the given expression.
   *
   * @param sym_table the symbol table to use
   * @param exist_pos the position of the existential to replace
   * @param equal_exp the expression to replace the existential with
   * @return an inequality constraint with the existential replaced
   */
  SRInequality replaceExistential(SymbolTable* sym_table,int exist_pos,
                                  ExpVec equal_exp) const;
};

/*!
 * \class SRConjunction
 * \brief Class containing sets of all the equalities and inequalities
 *
 * This class holds two sets: one for the equalities and one for the
 * inequalities. By doing so, this class represents the exact constraints for
 * which was defined.
 */
class SRConjunction{
public:

  /*!
   * SRConjunction Constructor
   *
   * @param equal A set of all the equalities in the given expression
   * @param inequal A set of all the inequalities in the given expression
   * @param tups A list of all the variables involved with this Conjunction
   */
  inline SRConjunction(set<SREquality> equal, set<SRInequality> inequal,
                       list<TupleType>tups):
                       equalities(equal), inequalities(inequal),
                       tuplevars(tups){}

  ///Apply method used by the visitors to traverse the Set/Relation structure
  ///@param visitor Visitor that is traversing the structure
  void apply(SRVisitor* visitor) const;

  ///Helper method for traversing the Conjunctions' equalities
  ///@param visitor Visitor that is traversing the structure
  void applyEqualities(SRVisitor* visitor) const;

  ///Helper method for traversing the Conjunctions' inequalities
  ///@param visitor Visitor that is traversing the structure
  void applyInequalities(SRVisitor* visitor) const;

  ///Helper method for traversing the Conjunctions' TupleEntrys
  ///@param visitor Visitor that is traversing the structure
  void applyTuples(SRVisitor* visitor) const;

//  SRConjunction intersect(const SRConjunction& other);

  /*!
   * Operator <
   *
   * Checks in the following order:
   * \li this equality set size < op2 equality set size
   * \li this inequality set size < op2 inequality set size
   * \li this equality set < op2 equality set
   * \li this inequality set < op2 inequality set
   * This takes advantage of set's operator< overload
   * @param op2 the SRConjunction to compare this SRConjunction to.
   * @return true if this SRConjunction is 'smaller' than the other, false
             otherwise
   */
  const bool operator<(const SRConjunction& op2) const;

  /*!
   * Operator ==
   *
   * Checks in the following order:
   * \li this equality set size = op2 equality set size
   * \li this inequality set size = op2 inequality set size
   * \li this equality set = op2 equality set
   * \li this inequality set = op2 inequality set
   * This takes advantage of set's operator== overload
   * @param op2 the SRConjunction to compare this SRConjunction to.
   * @return true if this SRConjunction is equivalent than the other, false
             otherwise
   */
  const bool operator==(const SRConjunction& op2) const;

  ///Checks to see if the constraint lists are empty
  ///@return true if the constraint lists are empty, false otherwise
  const bool isEmpty() const;

  ///@return The start of the tuple var list involved with this conjunction
  inline const list<TupleType>::const_iterator tuplevarsBegin() const {
    return tuplevars.begin();
  }

  ///@return The end of the tuple var list involved with this conjunction
  inline const list<TupleType>::const_iterator tuplevarsEnd() const {
    return tuplevars.end();
  }

  ///@return The list of named tuple variables for this conjunction
  list<string> tupleVarNames() const;

  ///@return The beginning of the equality set involved with this conjunction
  inline const set<SREquality>::const_iterator equalitiesBegin() const {
    return equalities.begin();
  }

  ///@return The end of the equality set involved with this conjunction
  inline const set<SREquality>::const_iterator equalitiesEnd() const {
    return equalities.end();
  }

  ///@return The beginning of the inequality set involved with this conjunction
  inline const set<SRInequality>::const_iterator inequalitiesBegin() const {
    return inequalities.begin();
  }

  ///@return The end of the inequality set involved with this conjunction
  inline const set<SRInequality>::const_iterator inequalitiesEnd() const {
    return inequalities.end();
  }

  /*!
   * Used to compare two tuples that will be mapped to each other to make sure
   * they are the same value. This always starts with the first tuple of the
   * SRConjunction that is calling it. Used in Compose and Apply.
   * @param The SRConjunction to compare against
   * @param a starting location to compare from the others tuple list
   * @param an ending location to compare from the others tuple list
   * @return if the tuples match
   */
  bool check_for_matching_constants(SRConjunction op2, int other_start,
    int other_end) const;

  /*!
   * Used to create the new conjunctions tuple list
   * @param list of tuple types for this conjunctions tuples
   * @param list of tuple types for other conjunctions tuples
   * @param The starting location for the this list
   * @param The end location for the this list
   * @param The starting location for the other list
   * @param The end location for the other list
   * @return The new tuple list for the conjuntion
   */
  list<TupleType> make_new_tuple_list(list<TupleType> conj_tups_this,
    list<TupleType> conj_tups_other, int this_start, int this_end,
    int other_start, int other_end) const;

  /*!
   * Determines if any constraints have an existential variable at the top
   * level of terms (i.e. it's not an argument to a UFS).  If so, returns true,
   * false otherwise.  In the case where a top level existential was found, the
   * first argument is the position of the existential variable and the second
   * is an ExpVec that represents the expression the existential is equal to.
   *
   * @param sym_table the symbol table to use
   * @param equality_constraint out parameter, the constraint that contains the
   *        top level existential
   * @param exist_pos out parameter, the position of the existential variable
   * @param equal_exp out parameter, the expression the existential is equal to
   * @return true if an existential term is found, false otherwise
   */
  bool getTopExistEqualExp(SymbolTable const*const sym_table,
                           SREquality& equality_constraint,
                           int& exist_pos,ExpVec& equal_exp) const;

  /*!
   * Determines if any equality constraints have a UFS that contains an
   * existential variable (at some level of nesting), the function has a
   * coefficient of 1 and a single paramter,  and the function has a known
   * inverse in the given context.  If so, this method returns true, false
   * otherwise.  In the true case, the original and modified equality
   * constraints are returned in the output parameters.  The original constraint
   * is modified as follows to produce the modified constraint:
   *
   * orig_eq = exp1 = 1*f(exp2)
   * new_eq = f_inv(exp1) = exp2
   *
   * @param sym_table the symbol table to use
   * @param orig_eq out parameter, the original candidate equality constraint
   * @param new_eq out paramter, the modified equality constraint
   * @return true if a candidate equality constraint is found, false otherwise
   */
  bool getInvFuncCandidate(SymbolTable *sym_table,
                           IEGenLibContext context,
                           SREquality& orig_eq,SREquality& new_eq) const;

  /*!
   * Determines if any equality constraints have a UFS that contains its 
   * inverse UFS as a parameter in the form F(F_inv(param)), the outer function 
   * has a coefficient of 1 and a single paramter which is its inverse.
   * If so, this method simplifies F(F_inv(param))+expr in the expression to
   * param+exrp, and returns true, or false otherwise.  In the true case, the
   * original and modified equality constraints are returned in the output 
   * parameters.  The original constraint is modified as follows to produce the
   * modified constraint:
   *
   * orig_eq = exp1 = 1*f(1*f_inv(exp2))
   * new_eq = exp1 = exp2
   *
   * @param sym_table the symbol table to use
   * @param orig_eq out parameter, the original candidate equality constraint
   * @param new_eq out paramter, the modified equality constraint
   * @return true if a candidate equality constraint is found, false otherwise
   */
  bool getNestedInvFuncsCandidate(SymbolTable *sym_table,
                           IEGenLibContext context,
                           SREquality& orig_eq,SREquality& new_eq) const;

  /*!
   * Determine if any coefficients of the given type at the given position are
   * non-zero.
   *
   * @param type the type of term to examine
   * @param pos the position of the term to check for non-zero coefficients
   * @param sym_table the symbol table to use to recurse into UFCall parameters
   * @return true if any coefficients of the given type in the given position
   *         are non-zero, false otherwise.
   */
  bool any(SymType type,int pos,SymbolTable const*const sym_table=NULL) const;

  /*!
   * Applies the equality replacement simplification to the conjunction
   * as many times as possible.  Returns the simplified conjunction.
   *
   * @param sym_table the symbol table to use
   * @return the simplified conjunction
   */
  SRConjunction equalityReplacement(SymbolTable* sym_table) const;

  /*!
   * Applies the inverse function simplification to the given conjunction
   * as many times as possible.  Returns the simplified result.
   *
   * @param sym_table the symbol table to use
   * @param the conjunction to simplify
   * @return the simplified conjunction
   */
  SRConjunction inverseFunctionSimplify(SymbolTable* sym_table,
                                        IEGenLibContext context) const;

  /*!
   * Applies the functin(function_inve(expr)) simplification to the
   * given conjunction as many times as possible.  Returns the
   * simplified result.
   *
   * @param sym_table the symbol table to use
   * @param the conjunction to simplify
   * @return the simplified conjunction
   */
  SRConjunction NestingInvertedFunctionSimplify(SymbolTable* sym_table,
                                        IEGenLibContext context) const;

  /*!
   * @return a new conjunction with only the affine constraints that this conjunction
   *         contains
   */
  SRConjunction getAffineConjunction() const;

  /*!
   * @return a new conjunction with only the UFS constraints that this conjunction
   *         contains
   */
  SRConjunction getUFSConjunction() const;

private:
  ///Set of equalities
  set<SREquality> equalities;
  ///Set of inequalities
  set<SRInequality> inequalities;
  ///List of the values in the tuple var associated with this conjunction
  list<TupleType> tuplevars;
};

/*!
 * \class SparseConstraints
 *
 * \brief The class that holds the constraints, the symbol table, and the
 *        list of all the tokens.
 *
 * The purpose of this class, at the moment, is mostly as a wrapper class and
 * to be extended by set and relation, both of which will have their own special
 * behaviors dealing with the arity
 */
class SparseConstraints{
public:

  ///Apply method used by the visitors to traverse the Set/Relation structure
  ///@param visitor Visitor that is traversing the structure
  inline void applySymbolTable(SRVisitor* visitor) const
  { SymTable->apply(visitor); }

  ///@return The beginning of the conjunctions involved in this Set/Relation
  inline set<SRConjunction>::const_iterator conSetBegin() const
  { return ConSet.begin(); }

  ///@return The end of the conjunctions involved in this Set/Relation
  inline set<SRConjunction>::const_iterator conSetEnd() const
  { return ConSet.end(); }

  ///@return The total amounts from the symbol table
  inline const map<SymType, int> getTotals() const
  { return SymTable->getTotals(); }

  ///@return The string returned from BuildSparseConstraintsVisitor
  inline const string getBSCVstring() const {return BSCVstring;}

  ///@return The size of the conjunction set
  inline const int conSize() const {return ConSet.size();}

#if 0
  pair<SparseConstraints*,SparseConstraints*>
    mergeSymbolTables(SparseConstraints& other) const;
#endif

  void apply(SRVisitor* visitor) const;

  /*!
   * A function that checks the arities match
   * @param pointer to the sparse constraint to check with
   */
  void checkArity(SparseConstraints const& other) const;

  /*!
   * A function that checks the tuple elements are the same (var/const)
   * @param pointer to the sparse constraint to check with
   */
  void checkConstVarMatchforUnion(SparseConstraints const& other) const;

  /*!
   * A function that gets a list of the tuple names
   * @return list of tuple names
   */
  inline list<string> getTupleVarNames() const { return (this->conSetBegin())->tupleVarNames(); }

  /*!
   * A function that gets a list of the tuple input elements for relations
   * @return list of tuple names
   */
  list<string> getInputTupleVarNames() const;

  /*!
   * A function that gets a list of the tuple output elements for relations
   * @return list of tuple names
   */
  list<string> getOutputTupleVarNames() const;

  /*!
   * A function that gets a list of the tuple input elements for relations
   * @return list of tuple types
   */
  list<TupleType> getInputTupleVarTypes() const;

  /*!
   * A function that gets a list of the tuple output elements for relations
   * @return list of tuple types
   */
  list<TupleType> getOutputTupleVarTypes() const;

//protected:
  /*!
   * Sparse Constraints Constructor
   *
   * The sparse constraints constructor has logic involved with it to check that
   * the tuple variables that each SRConjunction has associated with it aligns
   * with the others so that the union operation can go smoothly. It is also
   * responsible for creating the symbol table involved by using the appropriate
   * visitors.
   * @param pres_form The string representation of the Presburger Form
   * @param isSet true if this SparseConstraints is a set
   * @param context The context of this SparseConstraints
   */
  SparseConstraints(string pres_form, bool isSet, IEGenLibContext context);

  /*!
   * SparseConstraints constructor for use by the operations when creating a
   * new set/relation.
   */
  inline SparseConstraints(SymbolTable* symTable, set<SRConjunction> conSet,
      int inArity, int outArity, bool isSet, IEGenLibContext context) :
      SymTable(symTable), ConSet(conSet), inArity(inArity), outArity(outArity),
      isSet(isSet), context(context) {}

  /*!
   * Sparse Constraints Destructor
   *
   * Deletes the symbol table on exit.
   */
  virtual ~SparseConstraints(){delete SymTable;}

  SparseConstraints(const SparseConstraints &spc);

  SparseConstraints& operator=(const SparseConstraints &spc);

  ///integer that holds the value of the in Arity
  int inArity;

  ///integer that holds the value of the out Arity
  int outArity;

  ///The symbol table that holds entries and values to each token involved
  SymbolTable* SymTable;

  ///The set of SRConjunction involved in the sparse constraint class
  set<SRConjunction> ConSet;

  ///The string returned from BuildSparseConstraintsVisitor
  string BSCVstring;

  string astDot;

  bool isSet;

  IEGenLibContext context;

  /*!
   * Performs the majority of the equality checking for sets and relations
   */
  bool operator==(SparseConstraints const& other) const;

  /*!
   * performs the actual union of two sparseconstraints by merging symbol
   * tables and adding the SRConjuntions
   * @param a pointer to the other sparseconstraint
   * @return a pointer to the new sparseConstraint that has had union performed
   * on it
   */
  pair<SymbolTable*,set<SRConjunction> > Union(
    SparseConstraints const& other) const;

  /*!
   * Simplifies the set/relation by:
   * 1) projecting each existential variable out of all UFS-containing constraints
   * 2) projecting each existential variable out of all affine constraints using ISL
   *
   * If projection of all existential variables fails, an exception is raised.
   *
   * @return a new symbol table and a simplified set of conjunctions
   */
  pair<SymbolTable*,set<SRConjunction> > simplify() const;

  /*!
   * Removes any unneeded STEs in the given symbol table.
   *
   * @param orig_symtable the original, unreduced symbol table
   * @return a new, reduced symbol table
   */
  SymbolTable* reduceSymTable(SymbolTable* orig_symtable,
                              set<SRConjunction> conjs,
                              map<string,string> &orig2reduced) const;

  /*!
   * Converts the given conjunctiions from the original to the reduced symbol
   * table using the given variable name map.
   *
   * @param orig_symtable the original, unreduced symbol table
   * @param reduced_symtable the reduced symbol table
   * @param orig2reduced mapping of tuple names (should be the identity map)
   * @param conjs the conjunctions to convert
   * @return the converted conjunctions
   */
  set<SRConjunction> convertToReduced(SymbolTable* orig_symtable,
                                      SymbolTable* reduced_symtable,
                                      map<string,string>& orig2reduced,
                                      set<SRConjunction> conjs) const;

  /*!
   * Separates the affine and UFS constraints of the given conjunction.  Uses
   * ISL to simplify the affine constraints.  Returns the combined simplifified
   * affine + original UFS constraints.
   *
   * @param conj the initial affine + UFS constraints
   * @param sym_table the symbol table for the given conjunction
   * @return the simplified affine + original UFS constraints
   */
  SRConjunction affineSimplify(SRConjunction conj,SymbolTable *sym_table) const;

  /*!
   * Interface with ISL to simplify the given affine formula string.
   *
   * @return a formula string that has been simplified
   */
  string islSimplify(string affine_formula_string) const;

//THINGS THAT ARE NEEDED FOR NEW JOINT CODE SECTION
// merged_symbol_table, this, other, old2newThis, old2newOther, this_start,
// this_end, other_start, other_end, other_match_in, other_match_out,
// exists_eq_this, exists_eq_other


  set<SRConjunction> getNewConjunctions(SymbolTable* merged_symbol_table,
                                        Relation const& other,
                                        map<string,string> old2newThis,
                                        map<string,string> old2newOther,
                                        int this_start, int this_end,
                                        int other_start, int other_end,
                                        int other_match_in, int other_match_out,
                                        list<TupleType> exists_eq_this,
                                        list<TupleType> exists_eq_other) const;
};

//Forward declaration of Relation
class Relation;

/*!
 * \class Set
 *
 * \brief A SparseConstraints class that represents a PresSet
 *
 * This class has one arity related to it to represent exactly what the
 * Tuple variables involved can look like in the conjunctions. Otherwise, at the
 * moment, it is a wrapper class similar to SparseConstraints.
 *
 * Representation example: {[x]:x < 100}
 */
class Set: public SparseConstraints{
public:
  //Allow SparseConstraints to access the protected Set constructor
  friend class SparseConstraints;
  friend class Relation;
  /*!
   * Set Constructor
   * @param pres_form The string representation of the Presburger Set
   * @param ar The arity of the tuple variables
   */
  inline Set(string pres_form, IEGenLibContext context=IEGenLibContext()):
             SparseConstraints(pres_form, true, context){};

//  inline ~Set(){delete SymTable;}

  ///Apply method used by the visitors to traverse the Set/Relation structure
  ///@param visitor Visitor that is traversing the structure
  void apply(SRVisitor* visitor) const;

  void applySpCon(SRVisitor* visitor) const;

  ///@return The arity of the tuple variable list involved
  inline int getArity() const{ return inArity; }

  ///@return The omega syntax version of the given Presberger Form and
  ///        constraints
  string get_isl() const;

  ///@return The dotty syntax version of the given Presberger Form and
  ///        constraints
  string get_dot();

  ///@return The dotty syntax version of the given Presberger Form's AST
  string getAST();

  ///@return true if this set is equal to the given set, false otherwise
  bool operator==(const Set& other) const;

  ///@return set of the two sets unioned together
  Set Union(Set const& other) const;

  ///@return symbolics from the context
  IEGenLibContext GetContext() const {return context;}

protected:
  /*!
   * Set Constructor for use by the operations.
   */
  inline Set(SymbolTable* symTable, set<SRConjunction> conSet, int arity,
        IEGenLibContext context):
             SparseConstraints(symTable,conSet,arity,0,true,context){};

  /*
   * Calls the common simplify implementation in SparseConstraints
   *
   * @return a simplified Set with all existential variables projected out
   */
  Set simplify() const;
};

/*!
 * \class Relation
 *
 * \brief A SparseConstraints class that represents a PresRelation
 *
 * This class has two arities related to it to represent exactly what both of
 * the tuple variables involved can look like in the conjunctions. Otherwise, at
 * the moment, it is a wrapper class similar to SparseConstraints.
 *
 * Representation example: {[x]->[y]:x < 100 and y > 0}
 */
class Relation: public SparseConstraints{
public:
  //Allow SparseConstraints to access the protected Relation constructor
  friend class SparseConstraints;

  /*!
   * Relation Constructor
   * @param pres_form The string representation of the Presburger Set
   * @param inar The arity of the incoming set of tuple variables
   * @param outar The arity of the outgoing set of tuple variables
   */
  inline Relation(string pres_form, IEGenLibContext context=IEGenLibContext()):
                  SparseConstraints(pres_form, false, context){};

//  inline ~Relation(){delete SymTable;}

  ///Apply method used by the visitors to traverse the Set/Relation structure
  ///@param visitor Visitor that is traversing the structure
  void apply(SRVisitor* visitor) const;

  void applySpCon(SRVisitor* visitor) const;

  ///@return The arity of the input tuple variable list involved
  inline int getInArity() const { return inArity; }

  ///@return The arity of the output tuple variable list involved
  inline int getOutArity() const { return outArity; }

  ///@return The omega syntax version of the given Presberger Form and
  ///        constraints
  string get_isl() const;

  ///@return The dotty syntax version of the given Presberger Form and
  ///        constraints
  string get_dot();

  ///@return The dotty syntax version of the given Presberger Form's AST
  string getAST();

  ///@return true if this relation is equal to the given relation, false otherwise
  bool operator==(Relation const& other) const;

  ///@return the inverse of this relation
  Relation Inverse() const;

  ///@return the Relation made of two relations composed together
  Relation Compose(Relation const& r2) const;

  ///@return relation of the two relations unioned together
  Relation Union(Relation const& other) const;

  ///@return Set where the given relation has been applied to this set
  Set Apply(Set const& other) const;

  ///@return symbolics from the context
  IEGenLibContext GetContext() const {return context;}
protected:
  /*!
   * Set Constructor for use by the operations.
   */
  inline Relation(SymbolTable* symTable, set<SRConjunction> conSet, int inArity,
        int outArity,IEGenLibContext context):
        SparseConstraints(symTable,conSet,inArity,outArity,true,context){};

  /*
   * Calls the common simplify implementation in SparseConstraints.
   *
   * @return a simplified Relation with all existential variables projected out
   */
  Relation simplify() const;
};

}//end namespace iegenlib

#endif /* SET_RELATION_H_ */
